$\forall$$x$$\in$dom($f$). $v$=$f$($x$) $\Rightarrow$  $P$($x$;$v$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$x$:$A$. $x$ $\in$ dom($f$) $\Rightarrow$ $P$($x$;$f$($x$))